The present invention relates to design verification of an LSI, and relates, more particularly, to a design verification device, a method and a memory medium therefor, for a large-scale and complex circuit, that is, a semiconductor integrated circuit for which a high-speed verification of function is required with high verification assurance.
In a logic design stage of a semiconductor integrated circuit, an event-driven simulator simulates how an event is being processed through a circuit. The event refers to a plurality of kinds of input signals prepared for a circuit to be verified.
A function verification method according to the event-driven simulator involves an extremely large number of events as a circuit scale of the integrated circuit becomes larger, which leads to an enormously long simulation time. As a result, a turn-around time of design becomes longer.
Further, when the event-driven simulator is used, a designer must consider a combination (event) of input signals to be applied to a circuit of which operation is to be verified. The designer prepares this event as a test vector for individual function of the circuit.
In verifying complex functions of a circuit, it has become impossible to manually prepare a test vector that covers all the functions of the circuit. Therefore, there has been a trend that the verification assurance of the even-driven simulator is lowered when it is used for verifying a large-scale circuit having complex functions. The test vector refers to an input signal applied to an LSI for testing the LSI.
On the other hand, formal verification has been attracting attention as a technique for solving the above-described problems of the event-driven simulator. The formal verification is a method of verifying a function of a designed circuit by using a logic equation obtained from a circuit description of the circuit. According to the formal verification, verification of a function is carried out using the logic equation that reflects the circuit design to be verified (function equivalence check). Therefore, this method requires no test vector, thus ensuring a 100% verification assurance.
The formal verification has mainly two kinds of techniques. A first technique is a one for directly converting the whole circuit into a logic equation. A second technique is a one for first splitting the circuit into small portions called logic cones (logic circuit groups) and then converting the individual logic cone units into individual logic equations. FIG. 1 illustrates concept of one logic cone. In other words, circuit portions corresponding to logic equations of a register output and an external input and output in the vicinity of a function block as a unit, are verified and compared respectively.
The above first technique has a problem in that a logic equation becomes too large to have a sufficient memory capacity, and it is practically impossible to apply this technique to an LSI. The second technique can solve this problem. However, according to the second technique, as the verification is carried out for each logic cone as a unit, there arises such a constraint that it is not possible to verify and compare the designs unless the registers included in the circuit are in the same construction.
For example, assume that there has arisen a portion of a circuit into which it is desired to insert a buffer from the needs of a timing adjustment, as a result of a transfer from a high-level design such as RT level design (Register Transfer level design) or the like, to a gate level description. In this case, it is possible to utilize the equivalence verifying function according to the formal verification, if it is possible to complete the design alteration without altering the register construction.
In other words, the formal verification is a tool that uses the equivalence verifying function of checking the equivalence of two circuits when there are design circuits of a higher-level circuit and a lower-level circuit in design flow. According to the formal verification, when a function is to be altered for correcting a bug, there are produced as outputs a portion where a disagreement of functions occurred and a combination of inputs at the time of the occurrence of the disagreement. Accordingly, the designer can cope with this alteration to some extent.
However, this formal verification involves no concept of time, from the nature of this verification that it logically converts the circuit description. Therefore, it is not possible to carry out a setting of an item for verification by regarding that a function altered by the designer is a known fact including the concept of time.
The formal verification is a tool using the equivalence verification function. Accordingly, it is difficult to cope with a design alteration, and the applicable range of the formal verification is limited according to the current design flow. At the time of an RT level designing, functions and register structures are altered frequently. Therefore, under the current circumstances, it is not possible to effectively introduce the formal verification into the high-level designing such as the RT level design which most requires the verification of functions.
In the light of the above-described situation, it is an object of the present invention to provide a design verification device, a method and a memory medium therefor, for a semiconductor integrated circuit, capable of effectively introducing the formal verification even in a higher-level design and capable of constructing a high-speed function verification environment with high verification assurance.
A design verification device, a method and a memory medium therefor, for a semiconductor integrated circuit, has a function verification system which has an input of a circuit description before an alteration and a circuit description after the alteration and identifies an altered portion according to a disagreed portion, wherein formal verification is carried out for a circuit description that can assure an agreement with a key point corresponding to an output of a register and an input and an output of a signal in the circuit descriptions before and after the alteration, and verification is carried out by utilizing an event-driven simulation for a circuit description that cannot assure an agreement or equivalence of the key point.
According to the present invention, formal verification is utilized for portions other than an altered portion in a semiconductor integrated circuit to be verified. Therefore, a high-speed verification of function can be achieved. Further, an event-driven simulation for cutting out only an altered portion is a high-speed operation. Accordingly, it is possible to obtain an environment under which it possible to achieve a high-speed verification of function in a large-scale integrated circuit (LSI).
The invention will be explained in more detail. According to a first aspect of the present invention, there is provided a design verification device for a semiconductor integrated circuit, the device including: a mechanism for identifying an altered portion according to a disagreed portion of the circuit description from input means for inputting a circuit description before an alteration and a circuit description after the alteration; and verification means by simulation for carrying out formal verification for a circuit description that can assure an agreement with a key point corresponding to an output of a register and an input and an output of a signal in the circuit descriptions before and after the alteration, and for carrying out verification by utilizing an event-driven simulation for a circuit description that cannot assure an agreement or equivalence of the key point in the circuit descriptions before and after the alteration.
According to a second aspect of the invention, there is provided a design verification device for a semiconductor integrated circuit, the device including: means for identifying an altered portion for mapping a key point corresponding to an output of a register and an input and an output of a signal in the input circuit descriptions before an alteration and after the alteration, setting as an external input and output a key point of which descriptions before and after the alteration agree with each other, the key point being closest to a disagreed portion between the descriptions before and after the alteration, and modularizing a circuit portion including the altered portion; verification means by simulation for verifying the modularized circuit portion in the circuit descriptions before and after the alteration respectively by utilizing an event-driven simulation; and means for formal verification for verifying the circuit except for the modularized circuit by utilizing formal verification for the circuit descriptions before and after the alteration respectively by reflecting only a node that has been regarded as the external input and output.
According to a third aspect of the invention, there is provided a design verification method for a semiconductor integrated circuit, the method including: a process of inputting a circuit description before an alteration and a circuit description after the alteration; a process of identifying an altered portion according to a disagreed portion; a process of carrying out formal verification for a circuit description that can assure an agreement of a key point corresponding to an output of a register and an input and an output of a signal in the circuit descriptions before and after the alteration; and a process of carrying out a verification utilizing an event-driven simulation for a circuit description that cannot assure an agreement or equivalence of the key point.
According to a fourth aspect of the invention, there is provided a design verification method for a semiconductor integrated circuit, the method including: a process for inputting a circuit description before an alteration and a circuit description after the alteration; a process for identifying an altered portion for mapping a key point corresponding to an output of a register and an input and an output of a signal in the above input circuit descriptions, setting as an external input and output a key point at a closest position of which circuit description before the alteration agrees with the circuit description after the alteration from a portion of disagreement between the circuit descriptions before and after the alteration, and modularizing a circuit portion including the altered portion; a verification process by simulation for verifying the modularized circuit portion in the circuit descriptions before and after the alteration respectively by utilizing an event-driven simulation; and a formal verification process for verifying the circuit except for the modularized circuit by utilizing formal verification for the circuit descriptions before and after the alteration respectively by reflecting only a node that has been regarded as the external input and output.
According to a fifth aspect of the invention, there is provided a memory medium, readable by computer, for storing at least a design verification program for a semiconductor integrated circuit, the program including: a process for inputting a circuit description before an alteration and a circuit description after the alteration; a process for identifying an altered portion for mapping a key point corresponding to an output of a register and an input and an output of a signal in the above input circuit descriptions, setting as an external input and output a key point of which descriptions before and after the alteration agree with each other, the key point being closest to a disagreed portion between the descriptions before and after the alteration, and modularizing a circuit portion including the altered portion; a verification process by simulation for verifying the modularized circuit portion in the circuit descriptions before and after the alteration respectively by utilizing an event-driven simulation; and a formal verification process for verifying the circuit except for the modularized circuit by utilizing formal verification for the circuit descriptions before and after the alteration respectively by reflecting only a node that has been regarded as the external input and output.
Additional objects and advantages of the invention will be set forth in the description which follows, and in part will be obvious from the description, or may be learned by practice of the invention. The objects and advantages of the invention may be realized and obtained by means of the instrumentalities and combinations particularly pointed out hereinafter.